Peano arithmetic

A system for representing {natural number}s

inductively using only two symbols, "0" (zero) and "S"

(successor).

This could be expressed as a {recursive} data type with the

following {Haskell} definition:

data Peano ◦ Zero | Succ Peano

The number three, usually written "SSS0", would be Succ (Succ

(Succ Zero)). Addition of Peano numbers can be expressed as a

simple syntactic transformation:

plus Zero n ◦ n

plus (Succ m) n ◦ Succ (plus m n)

(1995-03-28)